Inference at * 2 3 
Iof proof for Lemma decidable-filter:



1. T : Type
2. T List
3. u : T
4. v : T List
5. P:({x:T| (x  v)} ).
5. (xv. Dec(P(x)))  (L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x)))))
6. P : {x:T| (x  [u / v])} 
7. x[u / v]. Dec(P(x))
8. L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x))))
  L':T List. (L'  [u / v] & (x:T. (x  L')  ((x  [u / v]) & P(x)))) 

latex

 by ((Unfold `l_all` (-2)) 
CollapseTHEN (((InstHyp[u] (-2)) 
CollapseTHENA (Auto)))) 

latex

Co1: .....antecedent..... NILNIL

Co1: 7. x:T. (x  [u / v])  Dec(P(x))
Co1: 8. L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x))))
Co1:   (u  [u / v])
Co2: 

Co2: 7. x:T. (x  [u / v])  Dec(P(x))
Co2: 8. L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x))))
Co2: 9. Dec(P(u))
Co2:   L':T List. (L'  [u / v] & (x:T. (x  L')  ((x  [u / v]) & P(x))))
Co.

Definitions	xL. P(x), P  Q, Dec(P), x:A. B(x), x:A  B(x), x:A. B(x), x:AB(x), type List, Type, (x  l)
Lemmas	l member wf